package bcontractor.propositional.factories;

import bcontractor.api.SATReasoner;
import bcontractor.api.Sentence;
import bcontractor.api.SentenceSet;

/**
 * A factory for contraction cases
 * 
 * @author lundberg
 * 
 */
public class ContractionCaseFactory<S extends Sentence<S>> {

	private final SentenceSetFactory<S> sentenceSetFactory;

	private final SentenceFactory<S> sentenceFactory;

	private final SATReasoner<S> reasoner;

	/**
	 * Constructor
	 * 
	 * @param sentenceSetFactory sentenceSetFactory
	 * @param sentenceFactory sentenceFactory
	 * @param reasoner reasoner
	 */
	public ContractionCaseFactory(SentenceSetFactory<S> sentenceSetFactory, SentenceFactory<S> sentenceFactory, SATReasoner<S> reasoner) {
		this.sentenceSetFactory = sentenceSetFactory;
		this.sentenceFactory = sentenceFactory;
		this.reasoner = reasoner;
	}

	/**
	 * Creates a contraction case using the given factories
	 * 
	 * @return contraction case
	 */
	public ContractionCase<S> create() {
		while(true) {
			SentenceSet<S> sentences = this.sentenceSetFactory.create();
			if(reasoner.isSatisfiable(sentences)) {
				for(int retry = 0; retry < 1000; retry++) {
					S sentence = this.sentenceFactory.create();
					if(reasoner.entails(sentences, sentence)) {						
						return new ContractionCase<S>(sentences, sentence);
					}
				}
			}
		}
	}
}
